g, h:GrpSig. InjMonHom(g;h)  Type 

latex

Up	groups 1
Definitions of Statement	MonHom(M1,M2), InjMonHom(g;h)
Definitions	InjMonHom(g;h), t  T, x:A. B(x), , MonHom(M1,M2)
Lemmas	grp sig wf, grp car wf, inject wf, monoid hom wf